s:LOSet, a, b:|s|. ((b <s a))  (a  b) 

latex

Up	sets 1
Definitions of Statement	PosetSig, DSet, QOSet, POSet{i}, LOSet
Definitions	t  T, x:A. B(x), P & Q, x,y. t(x;y), P  Q, P  Q, P  Q, Order(T;x,y.R(x;y)), Linorder(T;x,y.R(x;y)), DSet, QOSet, POSet{i}, LOSet, x(s1,s2), , Preorder(T;x,y.R(x;y))
Lemmas	loset wf, set car wf, set lt is sp of leq, not functionality wrt iff, set leq wf, strict part wf, set lt wf, not wf, iff functionality wrt iff, linorder lt neg, decidable set leq, set eq wf, eqfun p wf, poset sig wf, dset properties, preorder wf, dset wf, qoset properties, anti sym wf, qoset wf, poset properties, connex wf, poset wf, loset properties